import {Parser} from './parser.js'

const article = `

environ
relations <, isPrime, |_|, cool;
operations + precedence 64, ' precedence 5;
operations * precedence 60, 0;
brackets [: :], (* *);

environ
type Real;
type Nat -> Real;
type Dummy;

pred cool;
pred Real < Real;
pred |_| Nat;
pred |_| Real, Real, Nat;
pred isPrime Nat;

func 0 -> Nat;
func Nat + Nat -> Nat;
func Nat, Nat + Nat, Nat -> Nat;
func Nat, Nat * Nat, Nat -> Nat;
func Nat * Nat -> Nat;
func Nat' -> Nat;
func Nat, Nat' -> Nat;
func [: Nat,Real :] -> Nat;
func [: Nat,Nat,Nat :] -> Nat;

reserve x,y,z for Real, m,n for Nat;

1: true implies true;
1: true implies false;
1: not false;
1: (false iff true) iff false;
1: (false iff true) implies false;
1: true & not (false iff true) implies false;
9: true & not true implies false;
1: true & (true implies true);
1: true & false or (false iff true);
1: true & for x, y, z holds true;
1: true & for x, y be Nat ex z st true;
1: true or  ex x st true iff true;
1: for n,y holds n < y;
1: ex n,m st (cool implies for n st cool holds not |_| [:n,m:]);
1: ex n,m st not |_| [:n,m:]''' + (n *m,n  )'   ''+ m'' '*n ' '';

        text
        cool implies (cool & cool & true) & (cool & true)
        proof
            assume true and 1: cool and false;
            thus 2: true;
            thus cool & cool & true by 1,2;
            thus cool & true by 1,2;
        qed;

`

const parser = new Parser(article)

parser.parse()
